Lambda the Ultimate

I wouldn't normally think a library is LtU material, but since this one lives at the intersection of embedded DSLs, process calculi, and a spotlight language, I think it fits: Communicating Scala Objects, Bernard Sufrin, Communicating Process Architectures 2008.

In this paper we introduce the core features of CSO (Communicating Scala Objects) – a notationally convenient embedding of the essence of occam in a modern, generically typed, object-oriented programming language that is compiled to Java Virtual Machine (JVM) code.

If you would like to play with it, the library can be downloaded here.

You can read the docs and download the C++ source here.

V8 is supposedly the main added value of Chrome, the newly announced Google browser.

Our discussion of the Chrome announcement enumerates some of the features of V8.

Here's a little light reading for your day-after-Labor-Day (or whatever yesterday was where you live): Unchecked Exceptions can be Strictly More Powerful than Call/CC, Mark Lillibridge and Olivier Danvy, 1999, Higher-Order and Symbolic Computation.

We demonstrate that in the context of statically-typed purely-functional lambda calculi without recursion, unchecked exceptions (e.g., SML exceptions) can be strictly more powerful than call/cc. More precisely, we prove that a natural extension of the simply-typed lambda calculus with unchecked exceptions is strictly more powerful than all known sound extensions of Girard’s Fω (a superset of the simply-typed lambda calculus) with call/cc. This result is established by showing that the first language is Turing complete while the later languages permit only a subset of the recursive functions to be written.

I have to say that on seeing the title I was surprised: I cut my functional teeth on Scheme and every baby Schemer sucks up the knowledge that call/cc lets you create all manner of flow control including exceptions. But, as the paper makes clear, that's not necessarily the case in a statically-typed context.

Edit: Citeseerx was not responding very well, here's an alternative URL for the paper.

Chris Lattner's post last week to cfe-dev, "Blocks" in Clang (aka closures), has generated a certain amount of enthusiasm, since Clang is, or will be, a compiler for C to LLVM (cf. LLVM 1.5 has been released!).

The representation of closures as blocks resembles the technique used for Poletto's 'C language; cf. the related discussion on The MetaC Language.

UpgradeJ: Incremental Typechecking for Class Upgrades, Gavin Bierman, Matthew Parkinson and James Noble.

One of the problems facing developers is the constant evolution of components that are used to build applications. This evolution is typical of any multi-person or multi-site software project. How can we program in this environment? More precisely, how can language design address such evolution? In this paper we attack two significant issues that arise from constant component evolution: we propose language-level extensions that permit multiple, co-existing versions of classes and the ability to dynamically upgrade from one version of a class to another, whilst still maintaining type safety guarantees and requiring only lightweight extensions to the runtime infrastructure. We show how our extensions, whilst intuitive, provide a great deal of power by giving a number of examples. Given the subtlety of the problem, we formalize a core fragment of our language and prove a number of important safety properties.

There has been an energetic discussion of API evolution in the forum, so when I saw this paper I thought it might be of interest to LtU readers.

Relational Parametricity and Units of Measure, Andrew J. Kennedy, POPL 1997.

Type systems for programming languages with numeric types can be extended to support the checking of units of measure. Quantification over units then introduces a new kind of parametric polymorphism with a corresponding Reynolds-style representation independence principle: that the behaviour of programs is invariant under changes to the units used. We prove this `dimensional invariance' result and describe four consequences.

The first is that the type of an expression can be used to derive equations which describe its properties with respect to scaling (akin to Wadler's `theorems for free' for
System F). Secondly there are certain types which are inhabited only by trivial terms. For example, we prove that a fully polymorphic square root function cannot
be written using just the usual arithmetic primitives. Thirdly we exhibit interesting isomorphisms between types and for first-order types relate these to the central theorem of classical dimensional analysis. Finally we suggest that for any expression whose behaviour is dimensionally invariant there exists some equivalent expression whose type reflects this behaviour, a consequence of which would be a full abstraction result for a model of the language.

There's a new release of F# coming out with support for measure types, and so I thought I'd post a link to Andrew's paper about the subject. Now, if you've done any physics or engineering, you're probably familiar with the fact that units can sometimes really strongly constrain what form your equations can take. If you studied dimensional analysis more carefully than I did, you might even have learned that this is a consequence of the Buckingham pi theorem -- you can prove that if you have an equation with n variables involving k physical units, you can recast it as an equation with (n - k) dimension-free variables. Kennedy shows that the analogue of this theorem for programs in his language is a form of parametricity result at first order, which is quite slick.

This paper reports the results of a qualitative field study of the scholarly writing, collaboration, information management, and long-term archiving practices of researchers in five related subdisciplines. The study focuses on the kinds of artifacts the researchers create in the process of writing a paper, how they exchange and store materials over the short term, how they handle references and bibliographic resources, and the strategies they use to guarantee the long term safety of their scholarly materials.

Not directly programming language related, but two things makes this paper relevant. First, many of the tools involved, especially those that really enhance productivity are language-based, or include DSLs (e.g., Latex, Bibtex, R (+Sweave) etc.). Second, many of us write papers, and as language geeks we surely crave great tools...

So, what is you ideal tool chest when it comes to doing and publishing research? And what do you actually use everyday?

Erlang's actor concurrency model is a good fit for a wide range of concurrent applications. One domain that would seem ideal is real-time control of concurrent physical processes. But as it stands right now Erlang is best suited for soft real-time applications - there's really nothing in the language or runtime geared towards hard real-time constraints. Towards Hard Real-Time Erlang talks about one piece of the puzzle: a hard real-time scheduler.

In the last decades faster and more powerful computers made possible to seriously take into account high–level and functional programming languages also for non–academic projects. Haskell, Erlang, O’CAML have been effectively exploited in many application fields, demonstrating how high–level languages can help in writing efficient, readable and almost bug–free code, rapidly stealing the prominent position gained in many fields by OO languages such as Java and C++. One of the fields where low–level imperative languages are still preferred to functional programming is that of hard real–time applications, since usually programmers (and managers) think that high–level languages are really not able to cope with the complex and critical requirements of real–time.

In this paper we propose an implementation of a hard real–time scheduler entirely written in Erlang, and perfectly integrated with the Erlang BEAM emulator. Performance analysis show that the proposed solution is effective, precise and efficient, while remaining really simple to use as expected by Erlang programmers.

The paper closes with mentions of two more pieces of the puzzle.

Real–time message passing will be introduced in a future version...

...

A solution to the unpredictable behaviour of garbage collection should be implemented before a really hard real–time scheduling can be done in Erlang.

Besides the scheduler, message passing, and garbage collector, what else do you think is needed before Erlang or something like it is a viable alternative in this domain? Or is the actor model really not such a great fit?

*Edit: Based on a comment from renox added closing quotes about message passing and garbage collector and added message passing to the editorial question.

A useful short article by Ben Brosgol in COTS Journal.

On the surface, Ada and Java offer similar features to support real-time embedded military applications. But under the hood, they differ significantly in their underlying philosophy...

All that said, the Java / Ada decision need not be either/or. Mixed-language programming is provided by Java through the Java Native Interface, and by Ada through a standard interfacing framework. The enhancements in Ada 2005 make such interfacing easier, and there is current implementation support for mixed Ada/Java development. In a large system it may make sense to program different components in different languages—for example, a user interface in Java, hard real-time elements in Ada—thus taking advantage of the strengths of both. Ada and Java, rather than competing in the embedded defense system arena, may turn out to be comrades in arms.

Ben Brosgol is an expert on both Ada and Java support for real time programming, and I've linked to his papers that provide more detailed analysis a few times in the past.

A compelling description of the features that make CL the king of the Perl-Python-Ruby-PHP-Tcl-Lisp language ;)

Lisp is often promoted as a language preferable over others because it has certain features that are unique, well-integrated, or otherwise useful.

What follows is an attempt to highlight a selection of these features of standard Common Lisp, concisely, with appropriate illustrations.